package bcontractor.propositional;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Comparator;
import java.util.List;

import org.apache.commons.lang.builder.EqualsBuilder;
import org.apache.commons.lang.builder.HashCodeBuilder;

import bcontractor.api.Sentence;

/**
 * A propositional sentence. Representation based on DIMACS format.
 * 
 * @author lundberg
 * 
 */
public class PropositionalSentence implements Sentence<PropositionalSentence> {

    private final int[][] clauses;

    private final int maxvar;

    /**
     * Constructor
     * 
     * @param label
     *            label
     */
    public PropositionalSentence(int[]... clauses) {
        this.clauses = clauses;
        this.sortLiterals();
        this.sortClauses();
        this.maxvar = this.computeMaxvar();
    }

    private int computeMaxvar() {
        int max = 1;
        for (int[] clause : this.clauses) {
            for (int literal : clause) {
                max = Math.max(max, Math.abs(literal));
            }
        }
        return max;
    }

    private void sortClauses() {
        Arrays.sort(this.clauses, new Comparator<int[]>() {
            @Override
            public int compare(int[] o1, int[] o2) {
                if (o1.length != o2.length) {
                    return (o1.length < o2.length) ? -1 : 1;
                }
                for (int i = 0; i < o1.length; i++) {
                    if (o1[i] != o2[i]) {
                        return (o1[i] < o2[i]) ? -1 : 1;
                    }
                }
                return 0;
            }
        });
    }

    private void sortLiterals() {
        for (int i = 0; i < this.clauses.length; i++) {
            Arrays.sort(this.clauses[i]);
        }
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public PropositionalSentence negate() {
        return new PropositionalSentence(this.createNegationClauses());
    }

    /**
     * Number of the max atom.
     * 
     * @return int
     */
    public int getMaxvar() {
        return this.maxvar;
    }

    /**
     * Obtains a reference to the inner integer matrix that store the clauses.
     * This vector should NOT be changed.
     * 
     * @return matrix of literals
     */
    public int[][] getClauses() {
        return this.clauses;
    }

    private int[][] createNegationClauses() {
        List<int[]> negativeClauses = new ArrayList<int[]>();
        int[] clauseBuffer = new int[this.clauses.length];
        this.negationRecursion(negativeClauses, clauseBuffer, 0);
        return negativeClauses.toArray(new int[negativeClauses.size()][]);
    }

    private void negationRecursion(List<int[]> negativeClauses, int[] clauseBuffer, int clauseIndex) {
        if (clauseIndex == this.clauses.length) {
            int[] clause = new int[clauseIndex];
            System.arraycopy(clauseBuffer, 0, clause, 0, clauseIndex);
            negativeClauses.add(clause);
        } else {
            for (int literal : this.clauses[clauseIndex]) {
                clauseBuffer[clauseIndex] = -literal;
                this.negationRecursion(negativeClauses, clauseBuffer, clauseIndex + 1);
            }
        }
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public boolean equals(Object obj) {
        if (!(obj instanceof PropositionalSentence)) {
            return false;
        }
        PropositionalSentence o = (PropositionalSentence) obj;
        return new EqualsBuilder().append(this.clauses, o.clauses).isEquals();
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public int hashCode() {
        return new HashCodeBuilder().append(this.clauses).toHashCode();
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public String toString() {
        StringBuilder builder = new StringBuilder();
        builder.append("PropositionalSentence:");
        for (int[] clause : this.clauses) {
            builder.append(" (");
            for (int i = 0; i < clause.length - 1; i++) {
                builder.append(clause[i]);
                builder.append(", ");
            }
            builder.append(clause[clause.length - 1]);
            builder.append(")");
        }
        return builder.toString();
    }
}
